00100	GIVEAX(INT1,¬(UUεI0));
00200	
00300	GIVEAX(INT2,I0E = DOMAIN TORD I0);
00400	
01100	GIVEAX(INT6,SUCCEεDOMAIN(TORD I0→→TORD I0));
01200	
01300	GIVEAX(INT7,PREDEεDOMAIN(TORD I0→→TORD I0));
01400	
01500	GIVEAX(INT8,EQUALEεDOMAIN(TORD I0→→(TORD I0→→RTV)));
01600	
01700	GIVEAX(INT85,RELATION EQUALE);
01800	
01900	GIVEAX(INT9,(∀ X)(XεI0 ⊃ β(SUCCE,X) = SUCC X));
02000	
02100	GIVEAX(INT10,β(SUCCE,UU)=UU));
02200	
02300	GIVEAX(INT11,(∀ X)(XεI0 ∧ X≠0 ⊃ β(PREDE,X) = PRED X));
02400	
02500	GIVEAX(INT12,β(PREDE,UU)=UU);
02600	
02700	GIVEAX(INT13,β(PREDE,0)=UU);
02800	
02900	GIVEAX(INT14,(∀ X)(∀ Y)(XεI0E ∧ YεI0E ⊃ ββ(X,EQUALE,Y) =
03000	IF X=UU ∨ Y=UU THEN UU ELSE (IF X=Y THEN T ELSE F)));